/*
 * Copyright 2011, 2012 Fabian Wenzelmann
 * 
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 * 
 * Recognition-Procedures-for-Boolean-Functions is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 * 
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.  If not, see <http://www.gnu.org/licenses/>.
 */

package de.wenzelmf.booleanFunction.lpb.combinatorial.splittingTree;

import org.w3c.dom.Document;
import org.w3c.dom.Element;

import de.wenzelmf.booleanFunction.dnf.Clause;
import de.wenzelmf.booleanFunction.dnf.ClauseFactory;
import de.wenzelmf.booleanFunction.dnf.DNF;
import de.wenzelmf.booleanFunction.dnf.DNFFactory;
import de.wenzelmf.booleanFunction.dnf.Literal;
import de.wenzelmf.booleanFunction.lpb.combinatorial.occurrencePattern.OccurrencePattern;
import de.wenzelmf.booleanFunction.lpb.combinatorial.occurrencePattern.OccurrencePatternFactory;
import de.wenzelmf.booleanFunction.lpb.util.LPBCombinatorialConstants;
import de.wenzelmf.booleanFunction.util.Tuple;

// TODO: aux nodes don't really need to calculate the occurrence pattern? is it neccessary to create them?

/**
 * Superclass for all nodes in a splitting tree.
 * 
 * Such a node always consists of a DNF and child / parent nodes in the tree.
 * 
 * @author Fabian Wenzelmann
 * @version 1.0
 */
public abstract class SplittingTreeNode
{
	/*
	 * The lower child (its 1-successor).
	 */
	protected transient SplittingTreeNode lowerChild;
	/*
	 * The upper child (its 0-successor).
	 */
	protected transient SplittingTreeNode upperChild;
	/*
	 * The lower parent.
	 */
	protected transient SplittingTreeNode lowerParent;
	/*
	 * The upper parent.
	 */
	protected transient SplittingTreeNode upperParent;
	/*
	 * The DNF of this node.
	 */
	protected DNF dnf;
	/*
	 * The column in the table where this node is located (depth in the tree).
	 */
	protected Integer column;
	/*
	 * The row in the table where this node is located (the top most node has value 0, the node below it 1 and so forth).
	 */
	protected Integer row;
	/*
	 * The occurrence patterns (for all variables that have not been split away yet). The variables
	 * are sorted according the relation on occurrence patterns.
	 */
	protected OccurrencePattern[] occurrencePatterns;
	/*
	 * The tree conext that gives us some information about the tree this node is used in.
	 */
	protected TreeContext context;
	/*
	 * If the nodes link method has already been called this value is set to true.
	 */
	protected boolean alreadySplit;

	/**
	 * Constructs a new SplittingTreeNode.
	 * 
	 * The column of this node (column again referring to the table representation, the depth in the tree)
	 * is calculated from the parent nodes if present, i.e. it uses the parents column and adds 1.
	 * If both parents are null the column is supposed to be 0. 
	 * 
	 * @param lowerParent The lower parent of the node (referring to the table representation).
	 * @param upperParent The upper parent of the node (referring to the table representation).
	 * @param dnf The DNF associated with this node.
	 * @param occurrencePatterns The occurrence patterns (for all variables that have not been split away yet),
	 * variables are sorted according the relation on occurrence patterns.
	 * @param context Information about the tree this node is used in.
	 * 
	 * The lowerParent or upperParent are allowed to be {@code null} if they don't exist.
	 */
	public SplittingTreeNode(SplittingTreeNode lowerParent,
			SplittingTreeNode upperParent, DNF dnf, OccurrencePattern[] occurrencePatterns, TreeContext context)
	{
		this.lowerParent = lowerParent;
		this.upperParent = upperParent;
		this.dnf = dnf;
		this.occurrencePatterns = occurrencePatterns;
		this.context = context;
		this.alreadySplit = false;
		
		if(lowerParent != null)
		{
			this.column = lowerParent.column + 1;
		}
		else if(upperParent != null)
		{
			this.column = upperParent.column + 1;
		}
		else
		{
			this.column = 0;
		}
		if(context != null)
		{
			this.row = context.addNode(this);
		}
		else
		{
			this.row = null;
		}
	}
	
	// TODO: comment sounds strange...
	/**
	 * This abstract method is used to create the successors of this node.
	 * 
	 * The variable that is split away is the first variable in the occurrence pattern array.
	 * 
	 * If this method has been called the two child nodes should not be null (the split method
	 * must created them).
	 * 
	 * This method is only called on nodes if there are still some variables to split away (i. e.
	 * the occurrence patterns in this nodes are not empty).
	 * If there is no variable to split away the behavior is not specified.
	 * 
	 * A call of this method sets the value of {@code alreadySplit} to {@code true}.
	 * 
	 * @param symmetryTest If this value is {@code true} a symmetry test should be performed when
	 * splitting away the variable.
	 * @param factory The occurrence pattern factory that is used to create the occurrence patterns
	 * for the new generated child nodes.
	 * @param variables The variable setting that gives us some global information about the variables.
	 * @param clauseFactory The clause factory that is used to create the clauses of the
	 * generated DNFs.
	 * @param dnfFactory The DNF factory that is used to create the new DNFs.
	 * 
	 * @throws NotSymmetricException If the variables are not symmetric (see paper of Smaus for details),
	 * this means that we cannot represent this DNF as a LPB.
	 */
	public abstract void split(boolean symmetryTest, OccurrencePatternFactory factory,
			VariableSetting variables, ClauseFactory clauseFactory, DNFFactory dnfFactory) throws NotSymmetricException;
	
	/**
	 * This method should return the type of this node, i.e. for a {@link MainNode} it simply returns
	 * "mainNode".
	 * 
	 * Because this value is for example used to write XML entries it should use lowerCamelCase.
	 * 
	 * @return Type of this node.
	 */
	public abstract String getType();
	
	/**
	 * Just calls the {@link #split(boolean, OccurrencePatternFactory, VariableSetting, ClauseFactory, DNFFactory)}
	 * method with the default factories as defined in {@link LPBCombinatorialConstants}.
	 * 
	 * @param symmetryTest If this value is {@code true} a symmetry test should be performed when
	 * splitting away the variable.
	 * @param variables The variable setting that gives us some global information about the variables.
	 * 
	 * @throws NotSymmetricException If the variables are not symmetric (see paper of Smaus for details),
	 * this means that we cannot represent this DNF as a LPB.
	 */
	public void split(boolean symmetryTest, VariableSetting variables) throws NotSymmetricException
	{
		this.split(symmetryTest, LPBCombinatorialConstants.defaultOPFactory, variables,
				LPBCombinatorialConstants.defaultClauseFactory, LPBCombinatorialConstants.defaultDNFFactory);
	}
	
	/**
	 * Calling this method will set the DNF and the occurrence patterns to null to save memory.
	 */
	public void destroyContent()
	{
		this.dnf = null;
		this.occurrencePatterns = null;
	}
	
	/**
	 * This method should return final if this node is a final node.
	 * 
	 * @return {@code true} if this node is a final node.
	 */
	public abstract boolean isFinal();
	
	/**
	 * Return the lower child of this node (referring to the table notation),
	 * that is the 1-successor.
	 * 
	 * @return The lower child of this node.
	 */
	public SplittingTreeNode getLowerChild()
	{
		return lowerChild;
	}
	
	/**
	 * Return the upper child of this node (referring to the table notation),
	 * that is the 0-successor.
	 * 
	 * @return The upper child of this node.
	 */
	public SplittingTreeNode getUpperChild()
	{
		return upperChild;
	}
	
	/**
	 * Return the lower parent of this node (referring to the table notation).
	 * 
	 * @return The lower parent.
	 */
	public SplittingTreeNode getLowerParent()
	{
		return lowerParent;
	}
	
	/**
	 * Return the upper parent of this node (referring to the table notation).
	 * 
	 * @return The upper parent.
	 */
	public SplittingTreeNode getUpperParent()
	{
		return upperParent;
	}
	
	/**
	 * The DNF associated with this node.
	 * 
	 * @return The DNF associated with this node.
	 */
	public DNF getDnf()
	{
		return dnf;
	}
	
	/**
	 * The column in the table where this node is located (depth in the tree).
	 * 
	 * @return The column of this node in the table.
	 */
	public Integer getColumn()
	{
		return column;
	}
	
	/**
	 * The row in the table where this node is located (the top most node has value 0, the node below it 1 and so forth).
	 * 
	 * @return The row of this node in the table.
	 */
	public Integer getRow()
	{
		return row;
	}
	
	/**
	 * Return a String representation of this node.
	 * 
	 * @return "NODE: " + dnf.toString()
	 */
	@Override
	public String toString()
	{
		return "NODE: " + dnf;
	}

	/**
	 * Return the occurrence patterns of the DNF in this node (for all variables that have
	 * not been split away yet there is an occurrence pattern).
	 * The variables are sorted according the relation on occurrence patterns.
	 * 
	 * If a given field is null it indicates that the variable does not occur in the DNF.
	 * 
	 * @return The occurrence patterns of the node's DNF.
	 */
	public OccurrencePattern[] getOccurrencePatterns()
	{
		return occurrencePatterns;
	}
	
	/**
	 * Split away the most important variable (first one in the occurrence pattern array).
	 * 
	 * As result it returns the DNF that is obtained by splitting away <i>k</i> variables, the
	 * resulting occurrence patterns and the information if the new DNF represents <i>true</i>
	 * or <i>false</i>.
	 * 
	 * @param k is either {@code 0} or {@code 1}, if it is zero the result contains all clauses
	 * where this variable does not occur and otherwise all clauses where the variable occurs,
	 * but with this variable removed.
	 * @param factory The occurrence pattern factory that is used to create the occurrence
	 * patterns of the result. 
	 * @param variables The The variable setting that gives us some global information about
	 * the variables.
	 * @param clauseFactory The clause factory that is used to create the clauses of the resulting DNF.
	 * @param dnfFactory The DNF factory that is used to create the resulting DNF.
	 * 
	 * @return S(&Phi;, {x}, k) where <i>x</i> is the variable that is on the first position
	 * in the occurrence pattern array + additional information as defined in {@link SplitResult}. 
	 */
	// TODO: calculation of resIsFinal hasn't been tested yet, but should be obvious
	public SplitResult splitAway(int k, OccurrencePatternFactory factory,
			VariableSetting variables, ClauseFactory clauseFactory, DNFFactory dnfFactory)
	{
		Boolean resIsFinal = false;
		OccurrencePattern[] newOccurrences = new OccurrencePattern[ occurrencePatterns.length - 1 ];
		DNF newDnf = dnfFactory.getEmptyDNF(dnf.size());
		
		String variable = null;
		try
		{
			variable = occurrencePatterns[0].getVariable();
		}
		catch(NullPointerException e)
		{
			;
			// can happen if we don't have a variable in the DNF, i.e. the DNF is true or false
		}
		if(k == 0)
		{
			// create new DNF with all clauses that do not contain the variable
			for(Clause c : dnf)
			{
				if(!c.containsVariable(variable))
				{
					// create new clause, actualize occurrence pattern for all copied variables
					Clause newClause = clauseFactory.getEmptyClause(c.size());
					for(Literal l : c)
					{
						String name = l.getIdentifier();
						newClause.add(new Literal(name));
						// actualize occurrence pattern of this variable
						int position = variables.getPos(name);
						// TODO: correct??
						/*System.out.println("Try: " + (position - column));
						System.out.println("Size: " + newOccurrences.length);
						System.out.println(dnf);*/
						OccurrencePattern pattern = newOccurrences[position - column - 1];
						if(pattern == null)
						{
							pattern = factory.getEmptyInstance(name);
							newOccurrences[position - column - 1] = pattern;
						}
						pattern.addOccurrence(c.size());
					}
					newDnf.add(newClause);
					if(newClause.size() == 0)
					{
						resIsFinal = true;
					}
				}
			}
		}
		else
		{
			// create new DNF but remove the variable
			for(Clause c : dnf)
			{
				if(c.size() == 0)
				{
					// we found an empty clause. So return splitAway(0)
					newOccurrences = null;
					newDnf = null;
					return splitAway(0, factory, variables, clauseFactory, dnfFactory);
				}
				if(c.containsVariable(variable))
				{
					Clause newClause = clauseFactory.getEmptyClause(c.size());
					for(Literal l : c)
					{
						String name = l.getIdentifier();
						if(!name.equals(variable))
						{
							// add this literal
							newClause.add(new Literal(name));
							int position = variables.getPos(name);
							OccurrencePattern pattern = newOccurrences[position - column - 1];
							if(pattern == null)
							{
								pattern = factory.getEmptyInstance(name);
								newOccurrences[position - column - 1] = pattern;
							}
							pattern.addOccurrence(c.size() - 1);
						}
					}
					newDnf.add(newClause);
					if(newClause.size() == 0)
					{
						resIsFinal = true;
					}
				}
			}
		}
		if(newDnf.size() == 0)
		{
			resIsFinal = true;
		}
		return new SplitResult(newDnf, newOccurrences, resIsFinal);
		//return new Tuple<DNF, OccurrencePattern[]>(newDnf, newOccurrences);
	}
	
	/**
	 * Does the same as {@link #splitAway(int, OccurrencePatternFactory, VariableSetting, ClauseFactory, DNFFactory)}
	 * but with default factories as defined in {@link LPBCombinatorialConstants}.
	 * 
	 * @param k is either {@code 0} or {@code 1}, if it is zero the result contains all clauses
	 * where this variable does not occur and otherwise all clauses where the variable occurs,
	 * but with this variable removed.
	 * @param variables The The variable setting that gives us some global information about
	 * the variables.
	 * 
	 * @return The same as {@link #splitAway(int, OccurrencePatternFactory, VariableSetting, ClauseFactory, DNFFactory)}.
	 * 
	 * @see #split(boolean, OccurrencePatternFactory, VariableSetting, ClauseFactory, DNFFactory)
	 */
	public SplitResult splitAway(int k, VariableSetting variables)
	{
		return splitAway(k, LPBCombinatorialConstants.defaultOPFactory, variables,
				LPBCombinatorialConstants.defaultClauseFactory, LPBCombinatorialConstants.defaultDNFFactory);
	}
	
	/**
	 * Creates both successors of this DNF by splitting away the most important variable
	 * (first in the occurrence pattern array).
	 * 
	 * It generates the nodes with the DNFs S(&Phi;, {x}, 0) and S(&Phi;, {x}, 1) where <i>x</i>
	 * is the first variable in the occurrence pattern array.
	 * It returns the DNFs together with their occurrence patterns + the information if the DNF
	 * represents <i>true</i> or <i>false</i>. 
	 * 
	 * @param factory The occurrence pattern factory that is used to create the occurrence
	 * patterns of the result.
	 * @param variables The The variable setting that gives us some global information about
	 * the variables.
	 * @param clauseFactory The clause factory that is used to create the clauses of the resulting DNF.
	 * @param dnfFactory The DNF factory that is used to create the resulting DNF.
	 * 
	 * @return S(&Phi;, {x}, 0) and S(&Phi;, {x}, 1).
	 */
	// TODO: calculation of resIsFinal hasn't been tested yet, but should be obvious
	public Tuple<SplitResult, SplitResult> splitBoth(OccurrencePatternFactory factory,
			VariableSetting variables, ClauseFactory clauseFactory, DNFFactory dnfFactory)
	{
		// TODO: one of the dnfs will not be used once containsEmptyClause becomes true, therefore don't create this DNF furthermore, maybe even set it to null
		DNF firstDNF = dnfFactory.getEmptyDNF(dnf.size());
		DNF secondDNF = dnfFactory.getEmptyDNF(dnf.size());
		OccurrencePattern[] newOccurrencesFirst = new OccurrencePattern[ occurrencePatterns.length - 1 ];
		OccurrencePattern[] newOccurrencesSecond = new OccurrencePattern[ occurrencePatterns.length - 1 ];
		String variable = null;
		try
		{
			variable = occurrencePatterns[0].getVariable();
		}
		catch(NullPointerException e)
		{
			;
			// can happen if we don't have a variable in the DNF, i.e. the DNF is true or false
		}
		boolean containsEmptyClause = false;
		boolean firstFinal, secondFinal;
		firstFinal = false;
		secondFinal = false;
		for(Clause c : dnf)
		{
			if(c.size() == 0)
			{
				containsEmptyClause = true;
			}
			if(c.containsVariable(variable))
			{
				Clause newClause = clauseFactory.getEmptyClause(c.size());
				for(Literal l : c)
				{
					if(!l.getIdentifier().equals(variable))
					{
						newClause.add(l);
						String name = l.getIdentifier();
						int position = variables.getPos(name);
						OccurrencePattern pattern = newOccurrencesSecond[position - column - 1];
						if(pattern == null)
						{
							pattern = factory.getEmptyInstance(name);
							newOccurrencesSecond[position - column - 1] = pattern;
						}
						pattern.addOccurrence(c.size() - 1);
					}
				}
				secondDNF.add(newClause);
				if(newClause.size() == 0)
				{
					secondFinal = true;
				}
			}
			else
			{
				firstDNF.add(c);
				if(c.size() == 0)
				{
					firstFinal = true;
				}
				// TODO: maybe there is a better way to create the new occurrence pattern?
				for(Literal l : c)
				{
					String name = l.getIdentifier();
					int position = variables.getPos(name);
					OccurrencePattern pattern = newOccurrencesFirst[position - column - 1];
					if(pattern == null)
					{
						pattern = factory.getEmptyInstance(name);
						newOccurrencesFirst[position - column - 1] = pattern;
					}
					pattern.addOccurrence(c.size());
				}
			}
		}
		if(firstDNF.size() == 0)
		{
			firstFinal = true;
		}
		if(secondDNF.size() == 0)
		{
			secondFinal = true;
		}
		if(containsEmptyClause)
		{
			//return new Tuple<Tuple<DNF, OccurrencePattern[]>, Tuple<DNF, OccurrencePattern[]>>(new Tuple<DNF, OccurrencePattern[]>(firstDNF, newOccurrencesFirst), new Tuple<DNF, OccurrencePattern[]>(firstDNF, newOccurrencesFirst));
			return new Tuple<SplitResult, SplitResult>(new SplitResult(firstDNF, newOccurrencesFirst, firstFinal), new SplitResult(firstDNF, newOccurrencesFirst, firstFinal));
		}
		else
		{
			//return new Tuple<Tuple<DNF, OccurrencePattern[]>, Tuple<DNF, OccurrencePattern[]>>(new Tuple<DNF, OccurrencePattern[]>(firstDNF, newOccurrencesFirst), new Tuple<DNF, OccurrencePattern[]>(secondDNF, newOccurrencesSecond));
			return new Tuple<SplitResult, SplitResult>(new SplitResult(firstDNF, newOccurrencesFirst, firstFinal), new SplitResult(secondDNF, newOccurrencesSecond, secondFinal));
		}
		//return new Tuple<Tuple<DNF, OccurrencePattern[]>, Tuple<DNF, OccurrencePattern[]>>( splitAway(0, factory, variables, clauseFactory, dnfFactory), splitAway(1, factory, variables, clauseFactory, dnfFactory) );
		
	}

	/**
	 * Creates both successors of this DNF by splitting away the most important variable
	 * (first in the occurrence pattern array).
	 * 
	 * It generates the nodes with the DNFs S(&Phi;, {x}, 0) and S(&Phi;, {x}, 1) where <i>x</i>
	 * is the first variable in the occurrence pattern array.
	 * It returns the DNFs together with their occurrence patterns + the information if the DNF
	 * represents <i>true</i> or <i>false</i>.
	 * 
	 * @param variables The The variable setting that gives us some global information about
	 * the variables.
	 * 
	 * @return S(&Phi;, {x}, 0) and S(&Phi;, {x}, 1) together with their occurrence patterns.
	 * 
	 * @see #splitBoth(OccurrencePatternFactory, VariableSetting, ClauseFactory, DNFFactory)
	 */
	public Tuple<SplitResult, SplitResult> splitBoth(VariableSetting variables)
	{
		return splitBoth(LPBCombinatorialConstants.defaultOPFactory, variables, LPBCombinatorialConstants.defaultClauseFactory,
				LPBCombinatorialConstants.defaultDNFFactory);
	}
	
	/**
	 * If the nodes {@link #split(boolean, OccurrencePatternFactory, VariableSetting, ClauseFactory, DNFFactory)} method has already been called this method returns {@code true}.
	 * 
	 * @return {@code true} if {@link #split(boolean, OccurrencePatternFactory, VariableSetting, ClauseFactory, DNFFactory)}
	 * has already been called.
	 */
	public boolean isAlreadySplit()
	{
		return alreadySplit;
	}
	
	/**
	 * Returns the tree context of this node, this means some information about the tree this
	 * node is contained in.
	 * 
	 * @return The context of this node.
	 */
	public TreeContext getContext()
	{
		return context;
	}
	
	/**
	 * Return a XML element representing this node as defined in the manual.
	 *  
	 * @param document The root document (use it to create the Element object).
	 * 
	 * @return An element representing this node as defined in the manual.
	 */
	public Element getXMLElement(Document document)
	{
		Element nodeEntry = document.createElement(getType());
		
		nodeEntry.setAttribute("rowID", "" + getRow());
		nodeEntry.setAttribute("dnf", getDnf().toSetString());
		nodeEntry.setAttribute("dnfSize", "" + getDnf().size());
		
		nodeEntry.setAttribute("upperParent", getUpperParent() == null ? "None" : "" + getUpperParent().getRow());
		nodeEntry.setAttribute("lowerParent", getLowerParent() == null ? "None" : "" + getLowerParent().getRow());
		
		nodeEntry.setAttribute("upperChild", getUpperChild() == null ? "None" : "" + getUpperChild().getRow());
		nodeEntry.setAttribute("lowerChild", getLowerChild() == null ? "None" : "" + getLowerChild().getRow());
		
		Element occurrencePatternEntry = document.createElement("occurrencePatterns");
		// for each occurrence pattern write the entry
		for(OccurrencePattern op : occurrencePatterns)
		{
			if(op == null)
			{
				// TODO: is this ok??
				continue;
			}
			occurrencePatternEntry.appendChild(op.getXMLElement(document));
		}
		nodeEntry.appendChild(occurrencePatternEntry);
		return nodeEntry;
	}
}
